package typechecker.walkers;

import java.util.HashMap;
import java.util.Map;

import typechecker.ConstraintGraph;
import typechecker.TypeCheckingException;
import typechecker.ast.Context;
import typechecker.ast.type.ForallType;
import typechecker.ast.type.FunctionType;
import typechecker.ast.type.TypeConstructor;
import typechecker.ast.type.TypeConstructorApplication;
import typechecker.ast.type.TypeExpression;
import typechecker.ast.type.TypeVariable;

/**
 * We use a mapping between free variables of the coresponding type expressions
 */
public class SubtypingConstraintGenerator {
	
	private static void cgenConstructorApplication(
			TypeConstructorApplication te1, TypeConstructorApplication te2,
			ConstraintGraph c, Map<TypeVariable, TypeVariable> eq, Context<TypeVariable> ctx) {
		TypeConstructor tc1 = te1.getCons();
		TypeConstructor tc2 = te2.getCons();
		
		/* same constructor */
		if(!tc1.equals(tc2)){
			throw new TypeCheckingException(tc1.getName() + " is incompatible with " + tc2.getName() + " in the subtype relation");
		}
		
		/* substage relation */
		c.addConstraint(tc1.getStage(), tc2.getStage());
		
		/* recurse on arguments */
		for( int i =0 ; i < te1.getParams().size(); i++){
			TypeExpression p1 = te1.getParams().get(i);
			TypeExpression p2 = te2.getParams().get(i);
		
			cgenImpl(p1, p2, c, eq, ctx);
		}
	}

	private static void cgenFunctionType(FunctionType te1, FunctionType te2, ConstraintGraph c, Map<TypeVariable, TypeVariable> eq, Context<TypeVariable> ctx) {
		cgenImpl(te2.getSrc(), te1.getSrc(),c, eq, ctx);
		cgenImpl(te1.getDest(), te2.getDest(),c, eq, ctx);
		
	}

	private static void cgenVariable(TypeVariable te1, TypeVariable te2, ConstraintGraph c, Map<TypeVariable, TypeVariable> eq, Context<TypeVariable> ctx) {
		/* variables should corespond to each other in the mapping */
		if( eq.get(te1) == te2 || eq.get(te2) == te1){
			return;
		}

		/* OR should be bound by the same binder */
		if( (te1.getName() == te2.getName()) && (ctx.lookup(te1.getName()) == ctx.lookup(te2.getName()))){
			return;
		}
		throw new TypeCheckingException("variables " + te1.preetyPrint() + ", " + te2.preetyPrint() + " are compatible in subtype relation");
	}

	private static void cgenForallType(ForallType te1, ForallType te2,
			ConstraintGraph c, Map<TypeVariable, TypeVariable> eq, Context<TypeVariable> ctx) {
		eq.put(te1.getQuant(), te2.getQuant());
		cgenImpl(te1.getBody() , te2.getBody(), c, eq, ctx);
		eq.remove(te1.getQuant());
	}
	
	private static void cgenImpl(TypeExpression te1, TypeExpression te2, ConstraintGraph c, Map<TypeVariable, TypeVariable> eq, Context<TypeVariable> ctx){
		/* The two type expression must have the same structure */
		if(! te1.getClass().equals(te2.getClass())){
			throw new TypeCheckingException(te1.preetyPrint() + " and " + te2.preetyPrint() + " have different structure");
		}
		if (te1 instanceof ForallType){
			cgenForallType((ForallType)te1, (ForallType)te2, c, eq, ctx);
		} else if ( te1 instanceof FunctionType){
			cgenFunctionType((FunctionType)te1,(FunctionType)te2, c, eq, ctx);
		} else if ( te1 instanceof TypeConstructorApplication){
			cgenConstructorApplication((TypeConstructorApplication) te1, (TypeConstructorApplication)te2, c, eq, ctx);
		} else if ( te1 instanceof TypeVariable){
			cgenVariable((TypeVariable)te1, (TypeVariable)te2, c, eq, ctx);
		}	
	}

	public static void cgen(TypeExpression te1, TypeExpression te2, ConstraintGraph c, Context<TypeVariable> ctx){
		cgenImpl(te1, te2, c, new HashMap<TypeVariable, TypeVariable>(),ctx);
	}
}
